/*
 * Atomic Predicates for Transformers
 * 
 * Copyright (c) 2015 UNIVERSITY OF TEXAS AUSTIN. All rights reserved. Developed
 * by: HONGKUN YANG and SIMON S. LAM http://www.cs.utexas.edu/users/lam/NRL/
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * with the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 1. Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimers.
 * 
 * 2. Redistributions in binary form must reproduce the above copyright notice,
 * this list of conditions and the following disclaimers in the documentation
 * and/or other materials provided with the distribution.
 * 
 * 3. Neither the name of the UNIVERSITY OF TEXAS AUSTIN nor the names of the
 * developers may be used to endorse or promote products derived from this
 * Software without specific prior written permission.
 * 
 * 4. Any report or paper describing results derived from using any part of this
 * Software must cite the following publication of the developers: Hongkun Yang
 * and Simon S. Lam, Scalable Verification of Networks With Packet Transformers
 * Using Atomic Predicates, IEEE/ACM Transactions on Networking, October 2017,
 * Volume 25, No. 5, pages 2900-2915 (first published as IEEE Early Access
 * Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
 * THE SOFTWARE.
 */
package transformer;

import java.io.IOException;
import java.io.PrintWriter;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;
import java.util.Map.Entry;

import common.BDDACLWrapper;

import java.util.Set;
import common.FWDAPSet;
import common.PositionTuple;

public class StateTransferAP extends AbstractStateTransfer{


    public StateTransferAP(Net net)
    {
        super(net);
    }

    /**
     * return the head state
     */
    public StateAP Traverse(PositionTuple startpt, PositionTuple endpt)
    {
        reset_reachsets();

        destination = endpt;
        StateAP startstate = new StateAP(startpt, new FWDAPSet(BDDACLWrapper.BDDTrue));
        Traverse_recur(startstate);
        return startstate;
    }

    public StateAP Traverse(PositionTuple startpt, PositionTuple endpt, FWDAPSet injected_pkts)
    {
        reset_reachsets();

        destination = endpt;
        StateAP startstate = new StateAP(startpt, injected_pkts);
        Traverse_recur(startstate);
        return startstate;
    }

    public StateAP Traverse(PositionTuple startpt)
    {
        return Traverse(startpt, null, new FWDAPSet(BDDACLWrapper.BDDTrue));
    }

    public StateAP Traverse(PositionTuple startpt, FWDAPSet injected_pkts)
    {
        return Traverse(startpt, null, injected_pkts);
    }

    @Override
    public AbstractState getNxtStateLink(AbstractState s, PositionTuple pt) {

        FWDAPSet faps = ((StateAP)s).getAPSet();
        StateAP nxts = new StateAP(pt, faps, s.getAlreadyVisited(), s.getPtAlreadyVisited());
        return nxts;
    }

    @Override
    public AbstractState getNxtStateFwd(Object iter_obj, AbstractState s) {
        Map.Entry<String, FWDAPSet> oneentry = (Entry<String, FWDAPSet>) iter_obj;
        PositionTuple fwdedpt = new PositionTuple(s.getPosition().getDeviceName(), oneentry.getKey());
        StateAP fwdeds = new StateAP(fwdedpt, oneentry.getValue(), s.getAlreadyVisited(), 
                s.getPtAlreadyVisited());

        return fwdeds;
    }

    @Override
    public Iterator getForwardingEntries(AbstractState s) {
        Box nxtd = net.getBox(s.getPosition().getDeviceName());
        if(nxtd == null)
        {
            return null;
        }
        FWDAPSet fwdaps = ((StateAP) s).getAPSet();
        HashMap<String, FWDAPSet> fwdset =  nxtd.ForwardAction(s.getPosition().getPortName(), fwdaps);
        return fwdset.entrySet().iterator();
    }

    public static void main (String[] args) throws IOException
    {
        NetworkAP n = new NetworkAP("i2");
        n.ap_first_iter();

        n.apc.computeExpressions();
        FWDAPSet.setUniverse(n.apc.getAllAP());

        for(Box b: n.boxes.values())
        {
            b.setaps(n.apc);
        }
        StateTransferAP stfer = new StateTransferAP(n);
        long start = System.nanoTime();
        StateAP hs = null;
        //for(int i = 0; i < 10000; i ++)
        {
            //hs = stfer.Traverse(new PositionTuple("kans","xe-0/1/1"), new PositionTuple("salt","ge-6/0/0"));
            hs = stfer.Traverse(new PositionTuple("kans","xe-0/1/1"));
        }
        long end = System.nanoTime();
        hs.printState();
        System.out.println(hs.tree_size()+" nodes");
        System.out.println((end - start)/1000000.0);
    }

    public static double compute_trees_anypkt(Net net, Set<PositionTuple> pts, PrintWriter pw, boolean show_stat)
    {

        StateTransferAP stfer = new StateTransferAP(net);
        int repeat = 10;
        long t1 = System.nanoTime();
        for (int i = 0; i < repeat; i++)
        {
            for(PositionTuple pt1 : pts)
            {
                StateAP hs = stfer.Traverse(pt1);      
                //hs.printState();
                // show statistics of tree
                if(show_stat){
                    TreeStat ts = new TreeStat(hs);
                    ts.ShowStat();
                }
            }
        }

        long t2 = System.nanoTime();
        double elapse_time = (t2-t1+0.0)/1000000.0/repeat;
        if(pw != null)
            pw.println(elapse_time);
        return elapse_time;
    }

    public static double compute_trees_anypkt(Net net, Set<PositionTuple> pts, PrintWriter pw)
    {
        return compute_trees_anypkt(net, pts, pw, false);
    }

    public static double compute_trees(Net net, Set<PositionTuple> pts, FWDAPSet injected_pkts, boolean show_stat)
    {
        StateTransferAP stfer = new StateTransferAP(net);
        int repeat = 1;
        long t1 = System.nanoTime();
        for (int i = 0; i < repeat; i++)
        {
            for(PositionTuple pt1 : pts)
            {
                FWDAPSet pkts = new FWDAPSet(injected_pkts);
                StateAP hs = stfer.Traverse(pt1, pkts);      
                //hs.printState();
                if(show_stat){
                    TreeStat ts = new TreeStat(hs);
                    ts.ShowStat();
                }
            }
        }

        long t2 = System.nanoTime();
        double elapse_time = (t2-t1+0.0)/1000000.0/repeat;

        return elapse_time;
    }

}
